(set-logic QF_ABV)
(set-info :source |
Ivan Jager <aij+nospam@andrew.cmu.edu>

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun mem_35_146 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun R_EBX_6_81 () (_ BitVec 32))
(declare-fun R_EAX_5_79 () (_ BitVec 32))
(declare-fun R_ESI_2_75 () (_ BitVec 32))
(declare-fun R_EBP_0_70 () (_ BitVec 32))
(declare-fun R_ESP_1_58 () (_ BitVec 32))
(assert (let ((?v_36 (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_146 (bvadd R_ESP_1_58 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_146 (bvadd R_ESP_1_58 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_146 (bvadd R_ESP_1_58 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_146 (bvadd R_ESP_1_58 (_ bv3 32)))) (_ bv24 32)))) (?v_0 (concat (_ bv0 24) (select mem_35_146 (_ bv134560552 32))))) (let ((?v_1 (bvand (bvsub ?v_0 (_ bv0 32)) (_ bv255 32))) (?v_2 (bvsub R_ESP_1_58 (_ bv4 32)))) (let ((?v_3 (bvsub ?v_2 (_ bv4 32)))) (let ((?v_4 (bvsub ?v_3 (_ bv4 32)))) (let ((?v_5 (store (store (store (store (store (store (store (store (store (store (store (store mem_35_146 (bvadd ?v_2 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_70 (_ bv24 32)))) (bvadd ?v_2 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_70 (_ bv16 32)))) (bvadd ?v_2 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_70 (_ bv8 32)))) (bvadd ?v_2 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_70)) (bvadd ?v_3 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_ESI_2_75 (_ bv24 32)))) (bvadd ?v_3 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_ESI_2_75 (_ bv16 32)))) (bvadd ?v_3 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_ESI_2_75 (_ bv8 32)))) (bvadd ?v_3 (_ bv0 32)) ((_ extract 7 0) R_ESI_2_75)) (bvadd ?v_4 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBX_6_81 (_ bv24 32)))) (bvadd ?v_4 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBX_6_81 (_ bv16 32)))) (bvadd ?v_4 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBX_6_81 (_ bv8 32)))) (bvadd ?v_4 (_ bv0 32)) ((_ extract 7 0) R_EBX_6_81))) (?v_46 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_1 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))))) (let ((?v_22 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134560456 32) (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134560456 32) (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134560456 32) (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134560456 32) (_ bv3 32)))) (_ bv24 32)))) (?v_44 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134560596 32) (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134560596 32) (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134560596 32) (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd (_ bv134560596 32) (_ bv3 32)))) (_ bv24 32))))) (let ((?v_16 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_22 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (?v_6 (bvadd R_EAX_5_79 (_ bv28 32))) (?v_27 ((_ extract 7 0) (bvlshr (_ bv0 32) (_ bv24 32))))) (let ((?v_26 (bvadd ?v_6 (_ bv3 32))) (?v_29 ((_ extract 7 0) (bvlshr (_ bv0 32) (_ bv16 32)))) (?v_28 (bvadd ?v_6 (_ bv2 32))) (?v_31 ((_ extract 7 0) (bvlshr (_ bv0 32) (_ bv8 32)))) (?v_30 (bvadd ?v_6 (_ bv1 32))) (?v_33 ((_ extract 7 0) (_ bv0 32))) (?v_32 (bvadd ?v_6 (_ bv0 32)))) (let ((?v_7 (store (store (store (store ?v_5 ?v_26 ?v_27) ?v_28 ?v_29) ?v_30 ?v_31) ?v_32 ?v_33)) (?v_13 (bvadd (_ bv134560580 32) (_ bv0 32))) (?v_12 (bvadd (_ bv134560580 32) (_ bv1 32))) (?v_11 (bvadd (_ bv134560580 32) (_ bv2 32))) (?v_9 (bvadd (_ bv134560580 32) (_ bv3 32)))) (let ((?v_8 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_7 ?v_13)) (bvshl (concat (_ bv0 24) (select ?v_7 ?v_12)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_7 ?v_11)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_7 ?v_9)) (_ bv24 32))))) (let ((?v_10 (bvsub ?v_8 (_ bv1 32)))) (let ((?v_14 (store (store (store (store ?v_7 ?v_9 ((_ extract 7 0) (bvlshr ?v_10 (_ bv24 32)))) ?v_11 ((_ extract 7 0) (bvlshr ?v_10 (_ bv16 32)))) ?v_12 ((_ extract 7 0) (bvlshr ?v_10 (_ bv8 32)))) ?v_13 ((_ extract 7 0) ?v_10))) (?v_15 (bvadd (bvadd (bvadd ?v_4 (_ bv4 32)) (_ bv4 32)) (_ bv4 32)))) (let ((?v_38 (bvadd ?v_15 (_ bv0 32))) (?v_40 (bvadd ?v_15 (_ bv1 32))) (?v_41 (bvadd ?v_15 (_ bv2 32))) (?v_42 (bvadd ?v_15 (_ bv3 32))) (?v_17 (concat (_ bv0 24) ((_ extract 7 0) (concat (_ bv0 24) (select ?v_5 (_ bv134560400 32))))))) (let ((?v_18 (bvand (concat (_ bv0 31) (ite (bvult ?v_17 (_ bv1 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 32)))) (let ((?v_20 (bvand ?v_18 (_ bv1 32)))) (let ((?v_19 (bvxor (bvxor (_ bv0 32) ?v_18) ?v_20)) (?v_21 (bvnot (bvsub (_ bv0 32) ?v_18)))) (let ((?v_24 (bvadd ?v_21 (_ bv2 32))) (?v_45 (bvneg (_ bv1 32))) (?v_23 (bvsub ?v_22 (_ bv1 32))) (?v_25 (bvadd ?v_44 (_ bv8 32)))) (let ((?v_43 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_23 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (?v_34 (store (store (store (store (store (store (store (store ?v_5 (bvadd ?v_25 (_ bv3 32)) ((_ extract 7 0) (bvlshr ?v_24 (_ bv24 32)))) (bvadd ?v_25 (_ bv2 32)) ((_ extract 7 0) (bvlshr ?v_24 (_ bv16 32)))) (bvadd ?v_25 (_ bv1 32)) ((_ extract 7 0) (bvlshr ?v_24 (_ bv8 32)))) (bvadd ?v_25 (_ bv0 32)) ((_ extract 7 0) ?v_24)) ?v_26 ?v_27) ?v_28 ?v_29) ?v_30 ?v_31) ?v_32 ?v_33))) (let ((?v_35 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_34 ?v_13)) (bvshl (concat (_ bv0 24) (select ?v_34 ?v_12)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_34 ?v_11)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_34 ?v_9)) (_ bv24 32))))) (let ((?v_37 (bvsub ?v_35 (_ bv1 32)))) (let ((?v_39 (store (store (store (store ?v_34 ?v_9 ((_ extract 7 0) (bvlshr ?v_37 (_ bv24 32)))) ?v_11 ((_ extract 7 0) (bvlshr ?v_37 (_ bv16 32)))) ?v_12 ((_ extract 7 0) (bvlshr ?v_37 (_ bv8 32)))) ?v_13 ((_ extract 7 0) ?v_37))) (?v_47 (bvadd R_EAX_5_79 (_ bv8 32)))) (let ((?v_48 (store (store (store (store (store (store (store (store ?v_5 (bvadd ?v_47 (_ bv3 32)) ((_ extract 7 0) (bvlshr (_ bv2 32) (_ bv24 32)))) (bvadd ?v_47 (_ bv2 32)) ((_ extract 7 0) (bvlshr (_ bv2 32) (_ bv16 32)))) (bvadd ?v_47 (_ bv1 32)) ((_ extract 7 0) (bvlshr (_ bv2 32) (_ bv8 32)))) (bvadd ?v_47 (_ bv0 32)) ((_ extract 7 0) (_ bv2 32))) ?v_26 ?v_27) ?v_28 ?v_29) ?v_30 ?v_31) ?v_32 ?v_33))) (let ((?v_49 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_48 ?v_13)) (bvshl (concat (_ bv0 24) (select ?v_48 ?v_12)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_48 ?v_11)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_48 ?v_9)) (_ bv24 32))))) (let ((?v_50 (bvsub ?v_49 (_ bv1 32)))) (let ((?v_51 (store (store (store (store ?v_48 ?v_9 ((_ extract 7 0) (bvlshr ?v_50 (_ bv24 32)))) ?v_11 ((_ extract 7 0) (bvlshr ?v_50 (_ bv16 32)))) ?v_12 ((_ extract 7 0) (bvlshr ?v_50 (_ bv8 32)))) ?v_13 ((_ extract 7 0) ?v_50)))) (= (_ bv1 1) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_0 (_ bv0 32)) (bvxor ?v_0 ?v_1)) (_ bv7 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvor ?v_46 (bvand (bvnot (_ bv0 1)) (bvand (bvor ?v_16 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_8 (_ bv1 32)) (bvxor ?v_8 ?v_10)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (ite (not (= ?v_36 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_14 ?v_38)) (bvshl (concat (_ bv0 24) (select ?v_14 ?v_40)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_14 ?v_41)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_14 ?v_42)) (_ bv24 32))))) (_ bv1 1) (_ bv0 1)))) (bvor (bvnot ?v_16) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_17 (_ bv1 32)) (bvxor ?v_17 (bvand (bvsub ?v_17 (_ bv1 32)) (_ bv255 32)))) (_ bv7 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor (_ bv0 32) ?v_19) (bvxor (_ bv0 32) (bvsub (bvsub (_ bv0 32) ?v_19) ?v_20))) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_21 (bvxor (_ bv2 32) ?v_45)) (bvxor ?v_21 ?v_24)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_22 (_ bv1 32)) (bvxor ?v_22 ?v_23)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvor ?v_43 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_35 (_ bv1 32)) (bvxor ?v_35 ?v_37)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (ite (not (= ?v_36 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_39 ?v_38)) (bvshl (concat (_ bv0 24) (select ?v_39 ?v_40)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_39 ?v_41)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_39 ?v_42)) (_ bv24 32))))) (_ bv1 1) (_ bv0 1)))) (bvor (bvnot ?v_43) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_44 (bvxor (_ bv40 32) ?v_45)) (bvxor ?v_44 (bvadd ?v_44 (_ bv40 32)))) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (_ bv0 1)))))))))))) (bvor (bvnot ?v_46) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_49 (_ bv1 32)) (bvxor ?v_49 ?v_50)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (ite (not (= ?v_36 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_51 ?v_38)) (bvshl (concat (_ bv0 24) (select ?v_51 ?v_40)) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_51 ?v_41)) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_51 ?v_42)) (_ bv24 32))))) (_ bv1 1) (_ bv0 1)))))))))))))))))))))))))))))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
